module Zeno.ProofLogic where

import Prelude ()
import StdImports
import Zeno.Clause

data Proof a
  = Proven !(ProofStep a) ![Proof a]
  | Disproven !(ProofStep a) ![Proof a]
  | Unknown
  deriving ( Eq, Ord, Functor, Foldable, Traversable )
  
data ProofStep a 
  = ProofStep   { proofStepName :: !String,
                  proofStepClause :: !(Maybe (Clause a)),
                  proofStepAdded :: ![Clause a] }
  deriving ( Eq, Ord, Functor, Foldable, Traversable )
        
addStep :: ProofStep a -> Proof a -> Proof a
addStep _ Unknown = Unknown
addStep step ps@(Proven {}) = Proven step [ps]
addStep step ps@(Disproven {}) = Disproven step [ps]
 
anyProven :: [Proof a] -> Proof a
anyProven ps = 
  case find proven ps of
    Just p -> p
    Nothing -> Unknown
    
anyKnown :: [Proof a] -> Proof a
anyKnown = fromMaybe Unknown . find (not . unknown)
  
proven :: Proof a -> Bool
proven (Proven {}) = True
proven _ = False

disproven :: Proof a -> Bool
disproven (Disproven {}) = True
disproven _ = False

unknown :: Proof a -> Bool
unknown Unknown = True
unknown _ = False

conjoinStep :: ProofStep a -> [Proof a] -> Proof a
conjoinStep a ps = 
  case find disproven ps of
    Just dis -> dis
    Nothing -> allProvenStep a ps
        
allProvenStep :: ProofStep a -> [Proof a] -> Proof a
allProvenStep a ps = 
  if all proven ps
    then Proven a ps
    else Unknown

instance Show a => Show (Proof a) where
  show = showProofs' . return
  
instance Show a => Show (ProofStep a) where
  show (ProofStep name cls added) =
    let cls_s = case cls of
          Nothing -> "True"
          Just cls -> show cls
    in "[" ++ name ++ "] " ++ cls_s

indentedBars :: Indented String
indentedBars = do
  bs <- ask
  return $ '\n' : (replicate bs ' ') ++ (replicate bs '>') 
    ++ (if bs > 0 then " " else "")
  
showProofStep :: Show a => ProofStep a -> Indented String
showProofStep ps@(ProofStep name maybe_cls added) = do
  let ps_s = show ps
  i <- indentation
  let added_s = concatMap (((i ++ " + ") ++) . show) added
  return (ps_s ++ added_s)

showProofs' :: Show a => [Proof a] -> String
showProofs' = flip runReader 0 . showProofs
  
showProofs :: Show a => [Proof a] -> Indented String
showProofs [] = return []
showProofs [p] = showProof p
showProofs proofs@(_ : _) = indent $ do
  proofs' <- mapM showProof proofs
  {-
  i <- indentation
  let longest_lines = map (maximum . map length . lines) $ proofs'
      longest_lines' = map (\x -> x - (2 * indent)) longest_lines
      top_spacers = map (flip replicate '\\') longest_lines'
      bot_spacers = map (flip replicate '/') longest_lines'
      spacers = top_spacers `zip` bot_spacers
      proofs'' = zipWith
        (\(ts, bs) p -> i ++ ts ++ p ++ i ++ bs) spacers proofs'
  -}
  return $ "\n" ++ intercalate "\n" proofs'

showProof :: Show a => Proof a -> Indented String
showProof Unknown = 
  return "Unknown"
showProof (Proven step ps) = do
  ps' <- showProofs ps
  i <- indentedBars
  bars <- ask
  step_s <- showProofStep step
  return $ i ++ step_s ++ ps'
showProof (Disproven step ps) = do
  ps' <- showProofs ps
  i <- indentedBars
  bars <- ask
  step_s <- showProofStep step
  return $ i ++ "not " ++ step_s ++ ps'
